Structural Design with Alloy

In this workshop we will learn how use the lightweight formal method Alloy to design software structures. Alloy also allows the specification of behavioural requirements, but in this introductory workshop we will focus only on the structural aspects.

The Alloy motto is that “everything is a relation”, so first we will learn how to model structures with this simple mathematical concept. Then we will learn how to specify requirements of such structures using the relational logic of Alloy. Finally we will learn how we can leverage such formal models to automate testing of data structure implementations.

What attendees will learn

• How to model and specify software structures in Alloy
• How to leverage Alloy formal models to automate the testing of data structure implementations

Requirements for the workshop

• Laptop
• Java to run the Alloy Analyzer
• Your favourite programming language, including a library for parsing XML files and a graph library to test

Agenda/Plan for the workshop

• 45m talk introduction to structural design with Alloy
• 45m hands-on practice on specifying structural requirements with relational logic using several specification challenges in the Alloy4Fun platform
• 15m demo showing how to use Alloy models to automate the testing of some graph functions of the networkx python library
• 45m hands-on practice on automating the test of some graph functions

Companies that use this technology

Its mainly used in Academia, but some companies (for example, Gapgemini) already use it.

Target audience roles

• Software architects
• Software developers